x:Id, k:Knd, ds:x:Id fp Type, da:a:Knd fp Type, f:(State(ds)Valtype(da;k)ds(x)?Void).
with declarations ds:dsda:daeffect of k(v) is x := f s v  MsgA 

latex

Definitions	MsgA, a:A fp B(a), with declarations ds:dsda:daeffect of k(v) is x := f s v, mk-ma, locl(a), Prop, x : v, IdDeq, State(ds), Valtype(da;k), 1of(t), f(x)?z, KindDeq, rcv(l,tg), 2of(t), , x:A. B(x), x. t(x), Id, IdLnk, t  T, Knd
Lemmas	fpf-empty wf, pi2 wf, rcv wf, Kind-deq wf, fpf-cap wf, pi1 wf, ma-valtype wf, IdLnk wf, id-deq wf, fpf-single wf, locl wf, ma-state wf, mk-ma wf, Id wf, Knd wf, fpf wf